(set-logic QF_RDL)
(set-info :source | SMT-COMP'06 Organizers |)
(set-info :smt-lib-version 2.0)
(set-info :category "check")
(set-info :status sat)
(set-info :notes |This benchmark is designed to check if the DP supports bignumbers.|)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(declare-fun x3 () Real)
(declare-fun x4 () Real)
(assert (and (<= (- x1 x2) (/ 1 1000000000000000000000000000000000)) (<= (- x2 x3) (/ 1 2000000000000000000000000000000011)) (<= (- x3 x4) (/ (- 1) 1000000000000000000000000000000000)) (<= (- x4 x1) (/ (- 1) 2000000000000000000000000000000012))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
